T:Type, eq:EqDecider(T), es:ES, x:Id, e:{e:E| @loc(e)(x:T)} . lastchange(x;e) loc e  

latex

Definitions	{x:A| B(x)} , lastchange(x;e), Unit, P  Q, P & Q, x changed before e, left + right, e loc e' , P  Q, A c B, if b then t else f fi , (last change to x before e), x:AB(x), loc(e), , , b, s = t, A, False, @i(x:T), E, t.1, Id, Atom$n, ES, EqDecider(T), b, x:A  B(x), Type, x:A. B(x), P  Q, t  T
Lemmas	es-le weakening eq, assert wf, not wf, bnot wf, bool wf, es-loc wf, es-dtype wf, last-change wf, es-E wf, last-change-property, es-causle-le, changed wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, event system wf, Id wf